package com.googlecode.kipler.satisfiability.completion.rule.individual;

import java.util.Iterator;

import com.googlecode.kipler.container.dl.ABox;
import com.googlecode.kipler.container.dl.BasicWcsInterpolationData;
import com.googlecode.kipler.container.dl.ConceptCategory;
import com.googlecode.kipler.container.dl.LabelManager;
import com.googlecode.kipler.container.dl.WcsData;
import com.googlecode.kipler.satisfiability.reasoner.ReasonerException;
import com.googlecode.kipler.syntax.concept.Concept;
import com.googlecode.kipler.syntax.concept.ConceptName;
import com.googlecode.kipler.syntax.formula.ConceptAssertion;
import com.googlecode.kipler.syntax.formula.Formula;

/**
 * 
 * @author İnanç Seylan
 * 
 */
public class LazyUnfoldingRule extends ABoxRule {
	private boolean applied;

	@Override
	public void apply() throws ReasonerException {
		applied = false;
		ABox abox = getWorld().getABox();
		for (Iterator<Concept> i = getIndividual().conceptIterator(
				ConceptCategory.ATOMIC); i.hasNext();) {
			Concept concept = i.next();
			ConceptName c = (ConceptName) concept;
			Concept unfoldedDesc = getWorld().getTBox().getUnfoldable()
					.getDescription(c);
			if (unfoldedDesc != null) {
				ConceptAssertion newCa = new ConceptAssertion(unfoldedDesc,
						getIndividual().getName());
				if (!abox.contains(newCa)) {
					WcsData wcsData = getWcs().getData();
					wcsData.getLogger().info(
							"WCS " + getWcs().getId()
									+ " Lazy unfolding rule: Adding " + newCa);
					Formula condition = new ConceptAssertion(c, getIndividual()
							.getName());
					wcsData.getDependencyManager().move(newCa, condition);

					if (getWcs().getReasoner().getProfile()
							.isInterpolationEnabled()) {
						LabelManager labelMan = ((BasicWcsInterpolationData) getWcs()
								.getData()).getLabelManager();
						labelMan.copyLabel(condition, newCa);
					}

					abox.add(newCa);
					applied = true;
				}
			}
		}
	}

	@Override
	public boolean isApplied() {
		return applied;
	}

}
